Section: New Results

A simple presentation of the effective Topos

Participants : Alexis Bernadet [Contact] , Stéphane Lengrand [(CNRS, Lix)] .

We introduce here an alternative definition of Hyland’s effective topos, based on a realizability framework with two levels of abstraction: a low level and a high level. With this definition, the proof that this framework forms a topos is almost as simple as proving that the category of sets is a topos. Moreover, the high level of the framework can be directly used as a model of higher-order intuitionistic systems. We can then craft a programming language based on topos theory, which can be given a constructive semantics. In such a programming language, we can only write functions that terminate, as in proof assistants like Coq, so the language cannot be Turing-complete. The main advantage of having a programming language based on topos theory over more usual intuitionistic systems such as Martin-Loef type theory is the notion of equality: it is extensional, has proof-irrelevance, and allows the axiom of unique choice.

This work has been presented at the Chocola-Ens Lyon seminar in December 2011.